UnivTrevesV1, Main, Exploration, bibRecord, 001398

Formally certified floating-point filters for homogeneous geometric predicates

Identifieur interne : 001398 ( Main/Exploration ); précédent : 001397; suivant : 001399

Formally certified floating-point filters for homogeneous geometric predicates

Auteurs : Guillaume Melquiond [France] ; Sylvain Pion [France]

Source :

Informatique théorique et applications : (Imprimé) [ 0988-3754 ] ; 2007.

RBID : Pascal:08-0190571

Descripteurs français

Pascal (Inist)
- Virgule flottante, Filtre, Arithmétique, Calcul automatique, Calcul numérique, Potentiel, Implémentation, Orientation, Vérification formelle, Algorithme, Preuve, Informatique théorique, Application, Prédicat, 68Q60, 68Wxx.
Wicri :
- topic : Preuve.

English descriptors

KwdEn :
- Algorithm, Application, Arithmetics, Computer theory, Computing, Filter, Floating point, Formal verification, Implementation, Numerical computation, Orientation, Potential, Proof.

Abstract

Floating-point arithmetic provides a fast but inexact way of computing geometric predicates. In order for these predicates to be exact, it is important to rule out all the numerical situations where floating-point computations could lead to wrong results. Taking into account all the potential problems is a tedious work to do by hand. We study in this paper a floating-point implementation of a filter for the orientation-2 predicate, and how a formal and partially automatized verification of this algorithm avoided many pitfalls. The presented method is not limited to this particular predicate, it can easily be used to produce correct semi-static floating-point filters for other geometric predicates.

Affiliations:

Links toward previous steps (curation, corpus...)

to stream PascalFrancis, to step Corpus: 000843
to stream PascalFrancis, to step Curation: 000592
to stream PascalFrancis, to step Checkpoint: 000695
to stream Main, to step Merge: 001525
to stream Main, to step Curation: 001398

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Formally certified floating-point filters for homogeneous geometric predicates</title>
<author><name sortKey="Melquiond, Guillaume" sort="Melquiond, Guillaume" uniqKey="Melquiond G" first="Guillaume" last="Melquiond">Guillaume Melquiond</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>Laboratoire de l'informatique du parallélisme, UMR 5668 CNRS, ENS Lyon, INRIA, UCBL, 46 allée d'Italie</s1>
<s2>69364 Lyon</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Auvergne-Rhône-Alpes</region>
<region type="old region" nuts="2">Rhône-Alpes</region>
<settlement type="city">Lyon</settlement>
</placeName>
</affiliation>
</author>
<author><name sortKey="Pion, Sylvain" sort="Pion, Sylvain" uniqKey="Pion S" first="Sylvain" last="Pion">Sylvain Pion</name>
<affiliation wicri:level="3"><inist:fA14 i1="02"><s1>INRIA Sophia-Antipolis, 2004 route des Lucioles, BP 93</s1>
<s2>06902 Sophia-Antipolis</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Provence-Alpes-Côte d'Azur</region>
<settlement type="city">Sophia-Antipolis</settlement>
</placeName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">08-0190571</idno>
<date when="2007">2007</date>
<idno type="stanalyst">PASCAL 08-0190571 INIST</idno>
<idno type="RBID">Pascal:08-0190571</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000843</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000592</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000695</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000695</idno>
<idno type="wicri:doubleKey">0988-3754:2007:Melquiond G:formally:certified:floating</idno>
<idno type="wicri:Area/Main/Merge">001525</idno>
<idno type="wicri:Area/Main/Curation">001398</idno>
<idno type="wicri:Area/Main/Exploration">001398</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Formally certified floating-point filters for homogeneous geometric predicates</title>
<author><name sortKey="Melquiond, Guillaume" sort="Melquiond, Guillaume" uniqKey="Melquiond G" first="Guillaume" last="Melquiond">Guillaume Melquiond</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>Laboratoire de l'informatique du parallélisme, UMR 5668 CNRS, ENS Lyon, INRIA, UCBL, 46 allée d'Italie</s1>
<s2>69364 Lyon</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Auvergne-Rhône-Alpes</region>
<region type="old region" nuts="2">Rhône-Alpes</region>
<settlement type="city">Lyon</settlement>
</placeName>
</affiliation>
</author>
<author><name sortKey="Pion, Sylvain" sort="Pion, Sylvain" uniqKey="Pion S" first="Sylvain" last="Pion">Sylvain Pion</name>
<affiliation wicri:level="3"><inist:fA14 i1="02"><s1>INRIA Sophia-Antipolis, 2004 route des Lucioles, BP 93</s1>
<s2>06902 Sophia-Antipolis</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Provence-Alpes-Côte d'Azur</region>
<settlement type="city">Sophia-Antipolis</settlement>
</placeName>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Informatique théorique et applications : (Imprimé)</title>
<title level="j" type="abbreviated">Inform. théor. appl. : (Imprimé</title>
<idno type="ISSN">0988-3754</idno>
<imprint><date when="2007">2007</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Informatique théorique et applications : (Imprimé)</title>
<title level="j" type="abbreviated">Inform. théor. appl. : (Imprimé</title>
<idno type="ISSN">0988-3754</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Algorithm</term>
<term>Application</term>
<term>Arithmetics</term>
<term>Computer theory</term>
<term>Computing</term>
<term>Filter</term>
<term>Floating point</term>
<term>Formal verification</term>
<term>Implementation</term>
<term>Numerical computation</term>
<term>Orientation</term>
<term>Potential</term>
<term>Proof</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Virgule flottante</term>
<term>Filtre</term>
<term>Arithmétique</term>
<term>Calcul automatique</term>
<term>Calcul numérique</term>
<term>Potentiel</term>
<term>Implémentation</term>
<term>Orientation</term>
<term>Vérification formelle</term>
<term>Algorithme</term>
<term>Preuve</term>
<term>Informatique théorique</term>
<term>Application</term>
<term>Prédicat</term>
<term>68Q60</term>
<term>68Wxx</term>
</keywords>
<keywords scheme="Wicri" type="topic" xml:lang="fr"><term>Preuve</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Floating-point arithmetic provides a fast but inexact way of computing geometric predicates. In order for these predicates to be exact, it is important to rule out all the numerical situations where floating-point computations could lead to wrong results. Taking into account all the potential problems is a tedious work to do by hand. We study in this paper a floating-point implementation of a filter for the orientation-2 predicate, and how a formal and partially automatized verification of this algorithm avoided many pitfalls. The presented method is not limited to this particular predicate, it can easily be used to produce correct semi-static floating-point filters for other geometric predicates.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
</country>
<region><li>Auvergne-Rhône-Alpes</li>
<li>Provence-Alpes-Côte d'Azur</li>
<li>Rhône-Alpes</li>
</region>
<settlement><li>Lyon</li>
<li>Sophia-Antipolis</li>
</settlement>
</list>
<tree><country name="France"><region name="Auvergne-Rhône-Alpes"><name sortKey="Melquiond, Guillaume" sort="Melquiond, Guillaume" uniqKey="Melquiond G" first="Guillaume" last="Melquiond">Guillaume Melquiond</name>
</region>
<name sortKey="Pion, Sylvain" sort="Pion, Sylvain" uniqKey="Pion S" first="Sylvain" last="Pion">Sylvain Pion</name>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Rhénanie/explor/UnivTrevesV1/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001398 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 001398 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Rhénanie
   |area=    UnivTrevesV1
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     Pascal:08-0190571
   |texte=   Formally certified floating-point filters for homogeneous geometric predicates
}}

This area was generated with Dilib version V0.6.31.
Data generation: Sat Jul 22 16:29:01 2017. Site generation: Wed Feb 28 14:55:37 2024

	Serveur d'exploration sur l'Université de Trèves
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur l'Université de Trèves

Formally certified floating-point filters for homogeneous geometric predicates

Formally certified floating-point filters for homogeneous geometric predicates

Source :

Descripteurs français

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri